(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxRelTRS could be proven to be
BOUNDS(1, n^2).
The TRS R consists of the following rules:
a(C(x1, x2), y) → C(a(x1, y), a(x2, C(x1, x2)))
a(Z, y) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Rewrite Strategy: INNERMOST
(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)
transformed relative TRS to TRS
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^2).
The TRS R consists of the following rules:
a(C(x1, x2), y) → C(a(x1, y), a(x2, C(x1, x2)))
a(Z, y) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Rewrite Strategy: INNERMOST
(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(C(z0, z1), z2) → C(a(z0, z2), a(z1, C(z0, z1)))
a(Z, z0) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
A(Z, z0) → c1
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c3
EQZLIST(Z, C(z0, z1)) → c4
EQZLIST(Z, Z) → c5
SECOND(C(z0, z1)) → c6
FIRST(C(z0, z1)) → c7
AND(False, False) → c8
AND(True, False) → c9
AND(False, True) → c10
AND(True, True) → c11
S tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
A(Z, z0) → c1
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c3
EQZLIST(Z, C(z0, z1)) → c4
EQZLIST(Z, Z) → c5
SECOND(C(z0, z1)) → c6
FIRST(C(z0, z1)) → c7
AND(False, False) → c8
AND(True, False) → c9
AND(False, True) → c10
AND(True, True) → c11
K tuples:none
Defined Rule Symbols:
a, eqZList, second, first, and
Defined Pair Symbols:
A, EQZLIST, SECOND, FIRST, AND
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 10 trailing nodes:
AND(True, False) → c9
AND(False, False) → c8
SECOND(C(z0, z1)) → c6
EQZLIST(C(z0, z1), Z) → c3
AND(False, True) → c10
AND(True, True) → c11
FIRST(C(z0, z1)) → c7
A(Z, z0) → c1
EQZLIST(Z, C(z0, z1)) → c4
EQZLIST(Z, Z) → c5
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(C(z0, z1), z2) → C(a(z0, z2), a(z1, C(z0, z1)))
a(Z, z0) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:
a, eqZList, second, first, and
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c, c2
(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(C(z0, z1), z2) → C(a(z0, z2), a(z1, C(z0, z1)))
a(Z, z0) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:
a, eqZList, second, first, and
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c, c2
(9) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
a(C(z0, z1), z2) → C(a(z0, z2), a(z1, C(z0, z1)))
a(Z, z0) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c, c2
(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
We considered the (Usable) Rules:none
And the Tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(A(x1, x2)) = [2] + [2]x1
POL(C(x1, x2)) = [2] + x1 + x2
POL(EQZLIST(x1, x2)) = [2] + [2]x1 + [2]x2 + [2]x22 + [2]x1·x2 + [2]x12
POL(c(x1, x2)) = x1 + x2
POL(c2(x1, x2)) = x1 + x2
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:none
K tuples:
A(C(z0, z1), z2) → c(A(z0, z2), A(z1, C(z0, z1)))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
Defined Rule Symbols:none
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c, c2
(13) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(14) BOUNDS(1, 1)